| Definitions | False,   x. t(x), Prop, Id, EqDecider(T),  , Unit, t  T, IdLnk, Top, Knd, eventtype(k;loc;V;M;e), Msg_sub(l;M), Msg(M), haslink(l;m), mlnk(m), isrcv(k), isl(x), {i..j }, i  j < k, AB, ||as||, Y, lnk(k), outl(x), ESAxioms(E;T;M;loc;kind;val;when;after;sends;sender;index;first;pred;causl), Trans x,y:T. E(x;y), SWellFounded(R(x;y)), l[i], hd(l), nth_tl(n;as), if b t else f fi, ij,  b, i<j, tl(l), msg(l;t;v), tag(k), 2of(t), destination(l), source(l), ES, WellFnd{i}(A;x,y.R(x;y)), {T}, 1of(t), A, P   Q, E,  x:A. B(x), (e <loc e'), loc(e), P & Q, (e < e'), x(s) |